Nuprl Lemma : gcd_mul
2,24
postcript
pdf
a
,
b
,
n
:
. (
n
gcd(
a
;
b
)) ~ gcd(
n
a
;
n
b
)
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
gcd(
a
;
b
)
,
P
Q
,
GCD(
a
;
b
;
y
)
Lemmas
gcd
unique
,
gcd
p
mul
,
gcd
p
wf
,
gcd
wf
,
gcd
sat
pred
origin
a, b, n:
. (n
gcd(a;b)) ~ gcd(na;nb) a, b, n:. (ngcd(a;b)) ~ gcd(na;nb) x:A. B(x)
T
Q